In complex computer systems, multiple execution paths, or "threads" can be used to speed up processing. For example, interactions with users may be handled by foreground threads, while compute intensive operations such as database updates can be handled by background threads. Alternatively, parallel threads can be executed on multiple processors to improve performance.
It is a problem to detect concurrency errors. One type of concurrency error is a "deadly embrace," or a dead-lock condition. A dead-lock condition exists, for example, where a thread A "owns" a shared resource X, and also needs to acquire a resource Y. The resource Y is owned by a second thread B, which needs to acquire resource X. The result is a resource conflict. Typically, a dead-lock situation causes the system to stop functioning in its intended manner.
Another type of concurrency problem is a race condition. A race condition may exist if data states depend on the speed and order of thread execution. For example, a thread may need to read data at an address which can be written to by other threads. The actual data that are read will depend on the order of reading and writing by the individual threads. The non-determinism resulting from such race conditions can cause the program to produce erroneous results.
Prior art techniques are known to statically check for concurrency errors. Prior art techniques typically prove the theorem that the program is correct, or "true."
The problem is that an exact locking order, or data access sequence can vary dynamically while the threads are executing. Such variations are not detectable with a static checker. Therefore, it is desired to dynamically check for concurrency errors.